;; Copyright © 2016, cage
;; All rights reserved.

;; Redistribution and use in source and binary forms, with or without
;; modification, are permitted provided that the following conditions are met:

;;     * Redistributions of source code must retain the above copyright
;; notice, this list of conditions and the following disclaimer.
;;     * Redistributions in binary form must reproduce the above copyright
;; notice, this list of conditions and the following disclaimer in the
;; documentation and/or other materials provided with the distribution.

;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
;; AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
;; LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
;; CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
;; SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
;; CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
;; ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
;; THE POSSIBILITY OF SUCH DAMAGE.

(in-package :mu-kanren-goodies)

(defmacro zzz (fn)
  (with-gensyms (s/c)
    `(lambda-g (,s/c) (lambda-$ () (funcall ,fn ,s/c)))))

(defmacro bind-plus (binding g &rest rest)
  (if rest
      `(,binding (zzz ,g)
		 (bind-plus ,binding ,@rest))
      `(zzz ,g)))

(defmacro conj-plus (g &rest rest)
  `(bind-plus conj ,g ,@rest))

(defmacro disj-plus (g &rest rest)
  `(bind-plus disj ,g ,@rest))

(eval-when  (:execute :load-toplevel :compile-toplevel)
  (defun dummy-test (a b)
    (declare (ignore a b))
    t))

(define-constant +succeed+
  (lambda-g (subst)
    (unit subst))
  :test #'dummy-test)

(define-constant +fail+
  (lambda-g (subst)
    (declare (ignore subst))
    +mzero+)
    :test #'dummy-test)

(defmacro conde (&rest clauses)
  `(symbol-macrolet ((else +succeed+))
    (disj-plus ,@(loop for c in clauses collect `(conj-plus ,@c)))))

(defmacro fresh ((&rest vars) &body body)
  (if (null vars)
      `(conj-plus ,@body)
      `(call/fresh (lambda (,(first vars))
		     (declare (ignorable ,(first vars)))
		     (fresh (,@(rest vars)) ,@body)))))

(defun pull ($)
  (if (functionp $)
      (pull (funcall $))
      $))

(defun take-all ($)
  (let (($ (pull $)))
    (if (null $)
	'()
	(cons (car $)
	      (take-all (cdr $))))))

(defun take (n $)
  (if (zerop n)
      '()
      (let (($ (pull $)))
	(if (null $)
	    '()
	    (cons (car $)
		  (take (- n 1) (cdr $)))))))

(defun mk-reify (s/c*)
  (map 'list #'reify-state/1st-var s/c*))

(defun reify-state/1st-var (s/c)
  (let ((v (walk* (mu-var 0) (car s/c))))
    (walk* v (reify-subst v '()))))

(defun call/empty-state (g)
  (funcall g +empty-state+))

(defmacro run* ((&rest vars) &body body)
  `(mk-reify (take-all (call/empty-state (fresh ,(if vars
						     `(,@vars)
						     nil)
					   ,@body)))))

(defmacro run (n (&rest vars) &body body)
  (if (null n)
      `(run* ,vars ,@body)
      `(mk-reify (take ,n (call/empty-state (fresh ,(if vars
							`(,@vars)
							nil)
					      ,@body))))))

(defmacro %if-aux (name (&rest if-null) (&rest if-fn) (&rest if-t) &body body)
  `(labels ((,name ($)
	      (cond
		((null $)
		 ,@if-null)
		((functionp $)
		 ,@if-fn)
		(t
		 ,@if-t))))
     ,@body))

(defun ifte (g0 g1 g2)
  #'(lambda (s/c)
      (%if-aux fn
	       ((funcall g2 s/c))
	       ((lambda-$ () (fn (funcall $))))
	       ((bind $ g1))
	       (fn (funcall g0 s/c)))))

(defun once (g)
  #'(lambda (s/c)
      (%if-aux fn
	  (+mzero+)
	  ((lambda-$ () (fn (funcall $))))
	  ((list (car $)))
	(fn (funcall g s/c)))))
